r:, L:(Top List). ||nth_tl(r;L)|| = if r <z ||L|| then ||L|| - r else 0 fi    

latex

Definitions	x:A. B(x), nth_tl(n;as), if b then t else f fi , i <z j, t  T, Y, i z j, b, tt, ff, P  Q, i  j , A  B, A, False, P  Q, , P & Q, P  Q, T, True, tl(l), SQType(T), {T}, , , Unit, ||as||,
Lemmas	nat wf, nat properties, ge wf, lt int wf, length wf1, top wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of lt int, le int wf, le wf, bnot wf, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, non neg length, bnot of le int, tl wf, ifthenelse wf, length tl, nth tl wf, length nth tl, length cons